\noindent
The random generation of new species was one of the major problems that had to be resolved for the completion of this work.
This problem essentially reduces to randomly producing a set of unique proofs of a given proposition. Species are either grown
using a top down approach, or created from the mutation of an existing species. A maximal depth value on proofs \maxProofDepth{} is defined.
\newline
\newline
\noindent
The first step to the random generation of a set of new species is the identification of genes that may be used as propositions by the species.
This is done using the previously defined (6.2.2) $\mathit{type\_path}$ function.

\subsubsection{Generating an Initial Set of Potential Proofs}
\noindent
The function $\mathit{initialProofSet}$ uses the  $\mathit{type\_path}$ function to create
a list of proofs of a given type. Each proof generated by $\mathit{initialProofSet}$ is either a
proof in the form ($\mathit{Gene}\ \typ{ty}$) or a partial proof.
\begin{Program}[h]
\begin{verbatim}
initialProofSet [goal_type] genes =
\end{verbatim}
\begin{comment}
    $candidateTypes$ is extracted as a list of types $\typ{ty}$ in
    genes such that ($type\_path\ [ty]\ [goal\_type]$) holds;
\end{comment}
\begin{verbatim}
    let candidateTypes  =
        get_alleles genes (fun ty -> type_path ty goal_type)

    in map candidateTypes
    (fun ty ->
        match ty with
        | _ when ty_eqv ty goal_type --> Gene ty
        | TyAll sub_ty --> Partial (goal_type (TTelim (Gene ty) goal_type))
        | _ --> Partial (goal_type (Gene ty)))
\end{verbatim}
\caption{The $initialProofSet$ function}\label{initialProofSet}
\end{Program}
\noindent
The pseudo-code for the function is given in \ref{initialProofSet}. In it,  we note the use of the
following two functions (which will be seen again in other code listings):
\begin{enumerate}
\item the $get\_alleles$\index{get\_alleles} function takes a gene pool and a predicate on genes as arguments and returns a list of all the
alleles in the gene pool that are alleles of a gene that satisfies the argument predicate.
\item the $map$ function takes a list of objects of type $A$ and
a function $f$ of type $\AT{A}{B}$ as arguments and returns the list
resulting from the application of $f$ to each element of the
argument list.
\end{enumerate}
\begin{figure}[h]
\mbox{\epsfig{file=initialProofSetCall.eps}}
\caption{A call to the $\mathit{initialProofSet}$ function with goal type $\typ{Int}$} \label{initialProofSetCall}
\end{figure}
\noindent
Figure \ref{initialProofSetCall} illustrates a call to the  $\mathit{initialProofSet}$ function with the goal type argument $\typ{Int}$. In the case illustrated by the figure, the call returns four proofs, three of which are partial and one is complete. Given \GT, the call:
\begin{equation*}
\mathit{initialProofSet}\ \GT\ genes
\end{equation*}
\noindent
in which $genes$ is the name for the gene pool associated with the GP, provides a starting point
to the random generation of our initial set of proofs. Following this starting point, each proof in the list is separately passed as
argument to the $\mathit{modifyProof}$ function which takes a (possibly partial) proof as argument and returns a list of (possibly partial) proofs
generated from its modification. $\mathit{modifyProof}$ uses the $\mathit{get\_type}$ function which computes the
proposition (or type) that a proof proves. The pseudo-code for the $\mathit{get\_type}$ function is provided in program \ref{getType}.
\newline
\newline
\noindent \noindent Given a partial proof in the form
$(\mathit{Partial}\ \typ{Ty}\ \mathit{proof})$, we may suppose that
the following statements always hold true:
\begin{Program}
\begin{verbatim}
get_type proof =
   match proof with
   | Gene ty --> ty
   | TTelim sub_proof ty --> typeSubstTop (get_type sub_proof) ty
   | ->elim proof1 proof2 -->
        match ((get_type proof1),(get_type proof2)) with
        |((TyArr tyLeft tyRight) , tyArg)
            when (ty_eqv tyLeft tyArg) --> tyRight
        | _--> fail (proof is mal formed)
   | Partial ty _ --> ty
\end{verbatim}
\caption{The $get\_type$ function}\label{getType}
\end{Program}

\begin{enumerate}
\item $(\mathit{type\_path}\ (\mathit{get\_type}\ \mathit{proof})\ \typ{Ty})$ is always true
\item Given a proof $p = (\mathit{Partial}\ \typ{Ty}\ \mathit{proof})$, where $(ty\_eqv\ [Ty]\ (get\_type\ \mathit{proof}))$ is true, then $p$ may be replaced by simply be replaced by the proof $(\mathit{proof})$ of type $\typ{Ty}$ in any context.
\end{enumerate}
\noindent We are now almost ready to provide the pseudo-code for
$\mathit{modifyProof}$. The remaining discussion point pertains to
the stopping condition of the process. We may be able to generate
hundreds of proofs if we let the function go on for long enough, but
we only need to  generate enough species to produce enough genotypes
for our first generation. As we haven't introduced a formal
definition for genotypes yet (we do this in the next section), we
content ourselves to using a call to the function $enough\_genotypes$
which returns true when there are enough proofs to construct
the required number of genotypes. $enough\_genotypes$ lets the $\mathit{modifyProof}$
function know when it has produced enough proofs to generate the
first generation of the ecosystem $eco$. The $\mathit{modifyProof}$ function
also uses a $depth$ numeric argument, which
is the maximum depth in the proof tree at which
$\mathit{modifyProof}$ may still attempt to modify existing proofs.
We should note that $\mathit{modifyProof}$ might generate proofs
that already exist, in which case, they are excluded from the
resulting set of species. The commented pseudo-code is provided in
listing \ref{modifyProof}. $\mathit{modifyProof}$ uses the
$cartesianProduct$ function defined in \ref{cartesianProduct} with
signature:
\begin{equation*}
\mathit{cartesianProduct}:\AT{(\AT{A}{\AT{B}{C}})}{\AT{A\
list}{\AT{B\ list}{C\ list}}}
\end{equation*}
The $cartesianProduct$ function produces a list of all the
combination possibilities of two lists of objects using a
combination function.
\begin{Program}[h]
\begin{verbatim}
cartesianProduct combineFunc alist blist =
   let comb a = map (fun b -> combineFunc a b) blist in
   List.flatten (List.map (fun a -> comb a) alist)
\end{verbatim}
\caption{The $cartesianProduct$ function}\label{cartesianProduct}
\end{Program}
\noindent
Figure \ref{xhjs} illustrates the path that the algorithm
takes when it is given $\typ{Int}$ as its goal type argument, with
$Gene\typ{Int}$ as its starting proof.

%| pre condition: ty_eqv (get_type proof) [goal_type] is true      |
%| pre condition: depth >= 0                                       |
%| pre condition: depth <= \maxProofDepth                          |
\begin{Program}
\begin{verbatim}
modifyProof goal_type genes proof depth  =
match depth, proof with
\end{verbatim}
\begin{comment}
The following two sub-cases handle simplification of partial proofs
\end{comment}
\begin{verbatim}
    |(_, (Partial ty subproof)) when  ty_eqv (get_type subproof) ty -->
        modifyProof goal_type genes subproof depth
    | (_, (Partial _ partial_proof)) -->
        match get_type partial_proof with
                |TyArr ty1 ty2 ->
                    map (initialProofSet ty1 genes)
                    (fun pr -> modifyProof goal_type genes
                    (Partial (goal_type, ImplyElim (partial_proof, pr))) (depth -1))
                |TyAll ty -->
                    modifyProof goal_type (Partial (goal_type,
                    (TTelim (partial_proof, pr)))) (depth -1)
\end{verbatim}
\begin{comment}
The next sub-case's position in the list  of
clauses insures that it will not be a partial proof.
This case detects the argument as a complete proof, wraps it in a list and returnes it as result
\end{comment}
\begin{verbatim}
    | _ when ty_eqv (get_type proof) goal_type --> (proof::Nil)
\end{verbatim}
\begin{comment}
Next sub-case handles maximum depth reached. Can't go deeper
\end{comment}
\begin{verbatim}
    | 1, _ ->  initialProofSet goal_type genes
\end{verbatim}
\begin{comment}
Next sub-case: argument proof is a gene, but maximum depth is not reached, so
the node is branched out again.
\end{comment}
\begin{verbatim}
    |_ , (Gene ty) --> initialProofSet ty genes
\end{verbatim}
\begin{comment}
sub-case proof is \ImplyElim{}
\end{comment}
\begin{verbatim}
    |_, (->elim proof1 proof2)-->
            concatenate (initialProofSet goal_type)
                (cartesianProduct
                    (fun pr1 pr2 -> ImplyElim(pr1,pr2))
                    (modifyProof (get_type proof1) genes proof1 (depth - 1) )
                    (modifyProof (get_type proof2) genes proof2 (depth - 1) ))
\end{verbatim}
\begin{comment}
sub-case proof is \ForAllElim{}
\end{comment}
\begin{verbatim}
    | _, (TTelim subproof ty)-->
                concatenate (newProofs goal_type)
                (map (modifyProof (get_type subproof) genes subproof (depth - 1))
                (fun pr -> ForAllElim(pr,ty)))
\end{verbatim}
\caption{The $modifyProof$ function}\label{modifyProof}
\end{Program}


\begin{figure}
\centering \epsfig{file=proofDerivation.eps, width=\linewidth} \caption{A
trace of the $modifyProof$ (code \ref{modifyProof}) function when
initial argument is $\typ{Int}$} \label{xhjs}
\end{figure}
